n:, x, y:n. x before y  upto(n)  x<y 

latex

Definitions	Dec(P), P  Q, SQType(T), {T}, Unit, , b, b, if b t else f fi, i=j, t  ...$L, T, True, tl(l), ij, i<j, hd(l), x before y  l, L1  L2, P  Q, P  Q, S  T, S  T, l[i], i  j < k, AB, A, False, P  Q, Prop, t  T, ||as||, ij, upto(n), , x:A. B(x), increasing(f;k), {i..j}, x:A. B(x), P & Q
Lemmas	non neg length, nat wf, int seg wf, le wf, select wf, upto wf, length wf1, increasing wf, length upto, select upto, length cons, length nil, eq int wf, ifthenelse wf, assert wf, not wf, bnot wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, bool wf, decidable int equal